\section{Pattern Matching SELL} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\label{sec:pm}

A Semantically Enhanced Library Language is not a language of its own, but 
rather a sub-language embedded into another language -- C++ in our case. The 
sub-language still has the facilities we typically associate with programming 
languages e.g. syntax, semantics, type system, but they are constrained by
the host language. A particular sub-language can often be implemented in 
different host languages, which is why it is important to describe it 
independently of its host. We thus shall abstract from describing the 
exact syntax and semantics of host-language features that are well understood and documented 
elsewhere~\cite{C++11}.

\subsection{Syntax}
\label{sec:syn}

\begin{figure}[h]
\centering
\begin{tabular}{rcll}
\Rule{Match Statement}     & $M$       & \is{}  & \code{Match(}$e$\code{)} $\{ \left[C s^*\right]^* \}$ \code{EndMatch} \\
\Rule{Case Clause}         & $C$       & \is{}  & \code{Qua(}$T\left[,\varpi\right]^*$\code{)}\Alt{}\code{When(}$\varpi^*$\code{)}\Alt{}\code{Case(}$T\left[,x\right]^*$\code{)}\Alt{}\code{Otherwise(}$x^*$\code{)} \\
\Rule{Target Expression}   & $T$       & \is{}  & $\tau$ \Alt{} $l$ \\
\Rule{Layout}              & $l$       & \is{}  & $c^{\mathsf{int}}$ \\
\Rule{Match Expression}    & $m$       & \is{}  & $\pi(e)$ \\
\Rule{Extended Pattern}    & $\varpi$  & \is{}  & $\pi$ \Alt{} $c$ \Alt{} $x$ \\
\Rule{Pattern}             & $\pi$     & \is{}  & $\mu$ \Alt{} $\varrho$ \Alt{} $\eta$ \Alt{} $\chi$ \Alt{} $\varsigma$ \Alt{} $\_$ \\
\Rule{Constructor Pattern} & $\mu$     & \is{}  & \code{match<}$\tau\left[,l\right]$\code{>(}$\varpi^*$\code{)} \\
\Rule{Guard Pattern}       & $\varrho$ & \is{}  & $\pi \models \xi$ \\
\Rule{n+k Pattern}         & $\eta$    & \is{}  & $\xi$ \\
\Rule{Variable Pattern}    & $\chi^{\mathsf{variable}\langle\tau\rangle}$   \\
\Rule{Value Pattern}       & $\varsigma^{\mathsf{value}\langle\tau\rangle}$ \\
\Rule{Wildcard Pattern}    & $\_^{\mathsf{wildcard}}$                       \\
\Rule{Lazy Expression}     & $\xi$     & \is{}  & $\varsigma$ \Alt{} $\chi$ \Alt{} $\xi \oplus c$ \Alt{} $c \oplus \xi$ \Alt{} $\ominus \xi$ \Alt{} $(\xi)$ \Alt{} $\xi \oplus \xi$ \Alt{} $\varphi(\xi^*)$ \\
\Rule{Lazy Function}       & $\varphi^{\xi^*\rightarrow \xi}$ \\
\Rule{Unary Operator}      & $\ominus$ & $\in$  & $\lbrace*,\&,+,-,!,\sim\rbrace$ \\
\Rule{Binary Operator}     & $\oplus$  & $\in$  & $\lbrace*,/,\%,+,-,\ll,\gg,\&,\wedge,|,<,\leq,>,\geq,=,\neq,\&\&,||\rbrace$ \\
\Rule{Type-Id}             & $\tau$    &        & C++\cite[\textsection A.7]{C++11} \\
\Rule{Statement}           & $s$       &        & C++\cite[\textsection A.5]{C++11} \\
\Rule{Expression}          & $e^\tau$  &        & C++\cite[\textsection A.4]{C++11} \\
\Rule{Constant-Expression} & $c^\tau$  &        & C++\cite[\textsection A.4]{C++11} \\
\Rule{Identifier}          & $x^\tau$  &        & C++\cite[\textsection A.2]{C++11} \\
\end{tabular}
\caption{Abstract syntax of our pattern-matching SELL}
\label{syntax}
\end{figure}

Figure~\ref{syntax} presents the abstract syntax of our pattern-matching SELL. It presents 
the syntax embedded into the C++ without sacrificing 
the clarity of presentation. The idea is to show which interactions are possible 
within our SELL, while leaving the details of their implementation to 
\textsection\ref{sec:impl}. Where the specific technique we use to achieve such 
interactions crucially depends on the types of the entities involved,
we mention their type in the superscript. This dependence on the 
type system of the host language was also the reason why we chose abstract 
syntax over traditional EBNF. We make use 
of few non-terminals from the host language in order to put our constructs into 
context.

\emph{Match statement} is an analog of a switch statement with patterns as case 
clauses. Similar control structures exist in many programming languages and 
date back to at least Simula's Inspect statement~\cite{Simula67}.
In a library-based solution, we require it to be closed with a dedicated 
\code{EndMatch} macro, to properly close the syntactic structure 
introduced with \code{Match} and followed by \code{Case},\code{Qua} and 
\code{Otherwise} macros. Match statement will accept subjects of pointer and 
reference types, treating them uniformly in case clauses. This means that user 
does not have to mention \code{*,&} or any of the \code{const,volatile}-qualifiers
when specifying target types. Passing \code{nullptr} as a subject is considered 
\emph{ill-formed} however -- a choice we have made for performance reasons. 
Examples of match statement has already been presented in 
\textsection\ref{sec:intro} and \textsection\ref{sec:xmpl}.

We support four kinds of \emph{case clauses}: \code{Qua}, \code{When}, 
\code{Case}, and \code{Otherwise}.
The distinction between them is only important for the library 
implementation and can trivially be inferred in a compiler solution.
A \code{Qua}-clause is the most general clause taking an  
expression that identifies the target type as well as a list of extended 
patterns.
A \code{Qua}-clause permits nested patterns, but requires all the 
variables used in the patterns to be explicitly pre-declared. \code{Case}-clause 
only accepts simple patterns, conveniently introducing all the variables into the 
clause's scope. 
A \code{When}-clause takes only patterns while its target type is 
the subject type.
An \code{Otherwise} clause is an irrefutable clause that is 
semantically equivalent to \code{Case}-clause with subject type used as a target 
type. When used it should be the last clause of the match statement.
When default clause takes optional variable patterns, it behaves in 
exactly the same way as \code{Case} clause whose target type is the subject 
type.

A \emph{Target expression} is used by case clauses as either a target type, 
a constant value, representing \emph{layout} (\textsection\ref{sec:bnd}) or a 
\emph{view} type combining the two (\textsection\ref{sec:view}). The use of layout as target 
expression is only allowed for union encoding of algebraic data types 
(\textsection\ref{sec:unisyn}), in which case the library assumes the target 
type to be the subject type.

\emph{Views} in our library are represented by instantiations of a template class 
\code{view<T,l>} that takes a target type and a layout, combining the two into a 
new type. Our library takes care of transparent handling of this new type as the 
original combination of target type and layout. Views are discussed in details 
in~\textsection\ref{sec:view}.

\emph{Match expression} can be seen as an inline version of match statement with 
a single \code{Qua}-clause. Once a pattern is created, it can be applied to an 
expression in order to check whether that expression matches the pattern, 
possibly binding some variables in it. The result of application is always of 
type \code{bool} except for the tree pattern, where it is a value convertible to 
\code{bool}. The actual value in this case is going to be a pointer to target 
type \code{T} in case of a successful match and a \code{nullptr} otherwise. 
Match expressions will most commonly be seen to quickly decompose a possibly 
nested expression with a tree pattern as seen in the example in the paragraph 
below. They are the most used expressions under the hood however that let our 
library be composable. 

\emph{Pattern} summarizes \emph{applicative patterns} -- patterns that can be 
used in a match expression described above. For convenience reasons this 
category is extended with $c$ and $x$ to form an \emph{extended pattern} -- a
pattern that can be used as an argument of \emph{tree pattern} and \code{Qua} 
clause. Extended pattern lets us use constants as a \emph{value pattern} and 
regular C++ variables as a \emph{variable pattern} inside these constructs. The 
library implicitly recognizes them and transforms into $\varsigma$ and $\iota$ 
respectively. This transformation is further explained in~\textsection\ref{sec:aux} 
with $\stackrel{flt}{\vdash}$ rule set.

\emph{Tree pattern} takes a target type and an optional layout as its template 
arguments, which uniquely determines a concrete decomposition scheme for the 
type. Any nested sub-patterns are taken as run-time arguments. Besides 
applicative patterns, we allow constants and regular C++ variables to be passed 
as arguments to a tree pattern. They are treated as \emph{value patterns} and 
\emph{variable patterns} respectively. Tree patterns can be arbitrarily nested. 
The following example reimplements \code{factorize} from 
\textsection\ref{sec:bg} in C++ enhanced with our SELL:

\begin{lstlisting}
const Expr* factorize(const Expr* e)
{
    const Expr *e1, *e2, *e3, *e4;
    if (match<Plus>(match<Times>(e1,e2),match<Times>(e3,e4))(e))
        if (e1 == e3)
            return new Times(e1, new Plus(e2,e4));
        else
        if (e2 == e4)
            return new Times(new Plus(e1,e3), e4);
    return e;
}
\end{lstlisting}

\noindent
The above example instantiates a nested pattern and then immediately applies it 
to value \code{e} to check whether the value matches the pattern. If it does, 
it binds local variables to sub-expressions, making them available inside if.
Examples like this are known to be a week spot of visitor design pattern and we 
invite you to implement it with it in order to compare both solutions.

\emph{Guard patterns} in our SELL consist of two expressions separated by operator 
\code{|=}\footnote{Operator \code{|=} defining the guard was chosen arbitrarily 
from those that have relatively low precedence in C++. This was done to allow 
most of the other operators be used inside the condition without parenthesis}: 
an expression being matched (left operand) and a condition (right operand). The 
right operand is allowed to make use of the variable bound in the left operand. 
When used on arguments of a tree pattern, the condition is also allowed to make 
use of any variables bound by preceding argument positions. Naturally, a guard 
pattern that follows a tree pattern may use all the variables bound by the tree 
pattern. Consider for example decomposition of a color value, represented as a 
three-byte RGB triplet:

\begin{lstlisting}[keepspaces,columns=flexible]
variable<double> r,g,b;
auto p = match<RGB>( 
             255*r, 
             255*g |= g [<] r, 
             255*b |= b [<] g+r
         ) |= r+g+b <= 0.5;
\end{lstlisting}

\noindent
Note that C++ standard leaves the order of evaluation of functions arguments 
unspecified\cite[\textsection 8.3.6]{C++0x}, while we seem to rely here on 
\emph{left-to-right} order. The reason we can do this lays in the fact that for 
the purpose of pattern matching all the sub-expressions are evaluated lazily and 
the unspecified order of evaluation refers only to the order in which 
corresponding expression templates are created. The actual evaluation of these 
expression templates happens later when the pattern is applied to an expression 
and since at that point we have an entirely built expression at hand, we 
ourselves enforce its evaluation order.

Another important bit about our guards that has to be kept in mind is that 
guards depend on lazy evaluation and thus expression templates. This is why the 
variables mentioned inside a guard pattern must be of type \code{variable<T>} 
and not just \code{T}. Failing to declare them as such will result in eager 
evaluation of guard expression as a normal C++ expression. This will usually go 
unnoticed at compile time, while surprising at run time, especially to novices.

We chose to provide a syntax for guards to be specified on arguments of a tree 
pattern in addition to after the pattern in order to detect mismatches early 
without having to compute and either bind or match subsequent arguments.

\emph{n+k patterns} are essentially a subset of \emph{xt expressions} with at most 
one non-repeated variable in them. This allows for expressions like $2x+1$, but 
not for $x+x+1$, which even though is semantically equivalent to the first one, 
will not be accepted by our library as an \emph{n+k pattern}.

Expressions \code{255*r}, \code{255*g} and \code{255*b} in the example above 
were instances of our \emph{generalized n+k patterns}. Informally they meant the 
following: the value we are matching against is of the form $255*x$, what is the 
value of $x$? Since color components were assumed to be byte values in the range 
$\left[0-255\right]$ the user effectively gets normalized RGB coordinates in 
variables \code{r}, \code{g} and \code{b} ranging over $\left[0.0-1.0\right]$.

n+k pattern are visually appealing in the sense that they let us write code very 
close to mathematical notations often used in literature. Consider the definition 
of fast Fibonacci algorithm taken almost verbatim from the book. Function 
\code{sqr} here returns a square of its argument.

\begin{lstlisting}[keepspaces,columns=flexible]
int fib(int n)
{
    variable<int> m;
    Match(n)
    {
        When(1)     return 1;
        When(2)     return 1;
        When(2*m)   return sqr(fib(m+1)) - sqr(fib(m-1));
        When(2*m+1) return sqr(fib(m+1)) + sqr(fib(m));
    }
    EndMatch
}
\end{lstlisting}

\emph{Wildcard pattern} in our library is represented by a predefined global 
variable \code{_} of a dedicated type \code{wildcard} bearing no state. 
Wildcard pattern is accepted everywhere where a \emph{variable pattern} $\chi$ 
is accepted. The important difference from a use of an unused variable is that 
no code is executed to obtain a value for a given position and copy that value 
into a variable. The position is ignored altogether and the pattern matching 
continues.

There are two kinds of \emph{variable patterns} in our library: \emph{xt variable} 
and \emph{xt reference}. \emph{xt variable} stands for \emph{expression-template 
variable} and refers to variables whose type is \code{variable<T>} for any given 
type \code{T}. \emph{xt reference} is an \emph{expression-template variable 
reference} whose type is \code{var_ref<T>}. The latter is never declared 
explicitly, but is implicitly introduced by the library to wrap regular 
variables in places where our syntax accepts $x$. Both variable kinds are 
terminal symbols in our SELL letting us build expression templates of them. The 
main difference between the two is that \emph{xt variable} $\kappa$ maintains a 
value of type \code{T} as its own state, while \emph{xt reference} $\iota$ only 
keeps a reference to a user-declared variable of type \code{T}. Besides the 
difference in where the state is stored, both kinds of variables have the same 
semantics and we will thus refer to them as $\chi$. We will also use $\chi^\tau$ 
to mean either $\kappa^{variable\langle\tau\rangle}$ or 
$\iota^{var\_ref\langle\tau\rangle}$ since the type of the actual data $\tau$ is 
what we are interested in, while the fact that it was wrapped into 
\code{variable<>} or \code{var_ref<>} can be implicitly inferred from the 
meta-variable $\chi$. We would also like to point out that in most cases a 
variable pattern can be used as regular variable in the same context where a 
variable of type \code{T} can. In few cases where this does not happen 
implicitly, the user might need to put an explicit cast to \code{T&} or 
\code{const T&}.

\emph{Value pattern} is similarly never declared explicitly and is implicitly 
introduced by the library in places where $c$ is accepted.

\emph{xt expression} refers to an \emph{expression-template expression} -- a 
non-terminal symbol in our expression language built by applying a given 
operator to argument expression templates. We use this syntactic category to 
distinguish lazily evaluated expressions introduced by our SELL from eagerly 
evaluated expressions, directly supported by C++.

\emph{Layout} is an enumerator that user can use to define alternative bindings 
for the same class. When layout is not mentioned, the default layout is used, 
which is the only required layout a user has to define if she wishes to make use 
of bindings. We discuss layouts in details in \textsection\ref{sec:bnd}.

\emph{Binary operator} and \emph{unary operator} name a subset of C++ operators we 
make use of and provide support for in our pattern-matching library. 

The remaining syntactic categories refer to non-terminals in the C++ grammar 
bearing the same name. \emph{Identifier} will only refer to variable names in our 
SELL, even though it has a broader meaning in the C++ grammar. \emph{Expression}
subsumes any valid C++ expression. We use expression $e^\tau$ to refer to a C++ 
expression, whose result type is $\tau$. \emph{Constant-expression} is a subset 
of the above restricted to only expression computable at compile time. \emph{
Statement} refers to any valid statement allowed by the C++ grammar. Our match 
statement $M$ would have been extending this grammar rule with an extra case 
should it have been defined in the grammar directly. \emph{Type-id} represents a 
type expression that designates any valid C++ type. We are using this 
meta-variable in the superscript to other meta-variables in order to indicate a 
C++ type of the entity they represent.

\subsection{Bindings Syntax}
\label{sec:bnd}

Structural decomposition in functional languages is done with the help of 
constructor symbol and a list of patterns in positions that correspond to 
arguments of that constructor. C++ allows for multiple constructors in a class, 
often overloaded for different types but the same arity. Implicit nature of 
variable patterns that matches ``any value'' will thus not help in 
disambiguating such constructors, unless the user explicitly declares the 
variables, thus fixing their types. Besides, C++ does not have means for 
general compile-time reflection, so a library like ours cannot enumerate 
all the constructors present in a class automatically. This is why we decided to 
separate \emph{construction} of objects from their \emph{decomposition} through 
pattern matching with \emph{bindings}.

%Similarly to constructors, a class may have multiple deconstructors. Unlike 
%constructors, deconstructors are named differently.

The following grammar defines a syntax for a sublanguage our user will use to 
specify decomposition of various classes for pattern matching:\footnote{We reuse 
several meta-variables introduced in the previous grammar}

\begin{figure}
\begin{center}
\begin{tabular}{lp{1em}cl}
\Rule{bindings}                &           & \is{}  & $\delta^*$ \\
\Rule{binding definition}      & $\delta$  & \is{}  & \code{template <}$\left[\vec{p}\right]$\code{>} \\
                               &           &        & \code{struct bindings<} $\tau[$\code{<}$\vec{p}$\code{>}$]\left[,l\right]$\code{>} \\
                               &           &        & \code{\{} $\left[ks\right]\left[kv\right]\left[bc\right]\left[cm^*\right]$ \code{\};} \\
\Rule{class member}            & $cm$      & \is{}  & \code{CM(}$c^{size\_t},q$\code{);} \\
\Rule{kind selector}           & $ks$      & \is{}  & \code{KS(}$q$\code{);}    \\
\Rule{kind value}              & $kv$      & \is{}  & \code{KV(}$c$\code{);}    \\
\Rule{base class}              & $bc$      & \is{}  & \code{BC(}$\tau$\code{);} \\
\Rule{template-parameter-list} & $\vec{p}$ &        & C++\cite[\textsection A.12]{C++11} \\
\Rule{qualified-id}            & $q$       &        & C++\cite[\textsection A.4]{C++11} \\
\end{tabular}
\end{center}
\caption{Syntax used to provide bindings to concrete class hierarchy}
\label{fig:bindings}
\end{figure}

\noindent
Any type $\tau$ may have arbitrary amount of \emph{bindings} associated with it 
and distinguished through the \emph{layout} parameter $l$. The \emph{default 
binding} which omits layout papameter is implicitly associated with layout whose
value is equal to predefined constant \code{default_layout = size_t(}$\sim$\code{0)}. 
User-defined layouts should not reuse this dedicated value.

A \emph{Binding definition} consists of either full or partial specialization of a 
template-class:

\begin{lstlisting}
template <typename T, size_t l = default_layout>
    struct bindings;
\end{lstlisting}

\noindent
The body of the class consists a sequence of specifiers, which generate the 
necessary definitions for querying bindings by the library code. Note that 
binding definitions made this way are \emph{non-intrusive} since the original 
class definition is not touched. They also respect \emph{encapsulation} since 
only the public members of the target type will be accessible from within 
\code{bindings} specialization.

A \emph{Class Member} specifier \code{CM(}$c,q$\code{)} that takes (zero-based) binding 
position $c$ and a qualified identifier $q$, specifies a member, whose value will 
be used to bind variable in position $c$ of $\tau$'s decomposition with this 
\emph{binding definition}. Qualified identifier is allowed to be of one of the 
following kinds:

\begin{itemize}
\setlength{\itemsep}{0pt}
\setlength{\parskip}{0pt}
\item Data member of the target type
\item Nullary member-function of the target type
\item Unary external function taking the target type by pointer, reference or value.
\end{itemize}

\noindent
The following example definition provides bindings to the standard library type 
\code{std::complex<T>}:

\begin{lstlisting}[keepspaces,columns=flexible]
template <typename T> struct bindings<std::complex<T>> {
    CM(0, std::complex<T>::real); 
    CM(1, std::complex<T>::imag); 
};
\end{lstlisting}

\noindent
It states that when pattern matching against \code{std::complex<T>} for any 
given type \code{T}, use the result of invoking member-function \code{real()} to 
obtain the value for the first pattern matching position and \code{imag()} for 
the second position. 

In the presence of several overloaded members with the same name but different 
arity, \code{CM} will unambiguously pick one that falls into one of the three 
listed above categories of accepted members. In the example above, nullary 
\code{T std::complex<T>::real() const} is preferred to unary 
\code{void std::complex<T>::real(T)}.

Note that the binding definition above is made once for all instantiations of 
\code{std::complex} and can be fully or partially specialized for cases of 
interest. Non-parameterized classes will fully specialize the \code{bindings} 
trait to define their own bindings.

Using \code{CM} specifier a user defines the semantic functor 
$\Delta_i^{\tau,l},i=1..k$ we introduced in \textsection\ref{sec:semme} as 
following:

\begin{lstlisting}
template <> struct bindings<@$\tau$@> {
    CM(0, @$\tau$@::member_for_position_0); 
    ...
    CM(k, @$\tau$@::member_for_position_k); 
};
\end{lstlisting}

Note that binding definitions made this way are \emph{non-intrusive} since the 
original class definition is not touched. They also respect \emph{encapsulation} 
since only the public members of the target type will be accessible from within 
\code{bindings} specialization.

A \emph{Kind Selector} specifier \code{KS(}$q$\code{)} is used to specify a member 
of the subject type that will uniquely identify the variant for \emph{tagged} 
and \emph{union} encodings. The member $q$ can be of any of the three categories 
listed for \code{CM}, but is required to return an \emph{integral type}.

A \emph{Kind Value} specifier \code{KV(}$c$\code{)} is used by \emph{tagged} and 
\emph{union} encodings to specify a constant $c$ that uniquely identifies the 
variant.

A \emph{Base Class} specifier \code{BC(}$\tau$\code{)} is used by the \emph{tagged}
encoding to specify an immediate base class of the class whose bindings we 
define. A helper \code{BCS(}$\tau*$\code{)} specifier can also be used to 
specify the exact topologically sorted list of base classes 
(\textsection\ref{sec:cotc}).

A \emph{Layout} parameter $l$ can be used to define multiple bindings for the same 
target type. This is particularly essential for \emph{union} encoding where the 
types of the variants are the same as the type of subject and thus layouts 
become the only way to associate variants with position bindings. For this 
reason we require binding definitions for \emph{union} encoding always use the 
same constant $l$ as a kind value specified with \code{KV(l)} and the layout 
parameter $l$!

%The above definition will fall short, however, when we have to define bindings 
%for an algebraic data type encoded as \emph{discriminated union}. In this case 
%we have a single target type and multiple bindings associated with it. To 
%account for this, we recognize that a class (whether discriminated union or not)
%may have alternative bindings associated with it and thus introduce an optional 
%integral parameter called \emph{layout} that can be passed to \code{bindings} to
%distinguish various binding layouts. Classes that are not instances of our 
%discriminated union encoding are free to choose whatever unique constants they 
%feel appropriate to define alternative layouts. We require, however, that classes 
%representing discriminated union encoding use constants that correspond to kinds 
%supported by the union and only access members within layout that are valid for 
%its kind. 

Consider for example the following discriminated union describing various 
shapes:

\begin{lstlisting}[keepspaces,columns=flexible]
struct cloc { double first; double second; };
struct ADTShape
{
    enum shape_kind {circle, square, triangle} kind;
    union {
      struct { cloc center;     double radius; }; // circle
      struct { cloc upper_left; double size; };   // square
      struct { cloc first, second, third; };      // triangle
    };
};

template <> struct bindings<ADTShape> { 
    KS(ADTShape::kind);     // Kind Selector
};
template <> struct bindings<ADTShape, ADTShape::circle> {
    KV(ADTShape::circle);   // Kind Value
    CM(0, ADTShape::center);
    CM(1, ADTShape::radius);
};
\end{lstlisting}

\noindent
\code{KS} specifier within default bindings for \code{ADTShape} tells the library 
that value of a \code{ADTShape::kind} member, extracted from subject at run time, 
should be used to obtain a unique value that identifies the variant. Binding 
definition for \code{circle} variant then uses the same constant 
\code{ADTShape::circle} as the value of the layout parameter of the 
\code{bindings<T,l>} trait and \code{KV(l)} specifier to indicate its \emph{kind 
value}.

Should the shapes have been encoded with a \emph{Tag Class}, the bindings for 
the base class \code{Shape} would have contained \code{KS(Shape::kind)} 
specifier, while derived classes \code{Circle}, \code{Square} and 
\code{Triangle}, representing corresponding variants, would have had 
\code{KV(Shape::circle)} etc. specifiers in their binding definitions. These 
variant classes could have additionally defined a few alternative layouts for 
themselves, in which case the numbers for the layout parameter could have been 
arbitrarily chosen.

\subsection{Typing Rules}

\begin{figure}[h]
\begin{mathpar}

\inferrule[T-Var]
{}
{\Gamma\vdash \chi : \Variable{T}}

\inferrule[T-Value]
{}
{\Gamma\vdash \varsigma : \Value{T}}

\inferrule[T-Wildcard]
{}
{\Gamma\vdash \_ : \Wildcard}

\inferrule[T-Unary]
{\Gamma\vdash \xi : E}
{\Gamma\vdash \ominus \xi : \ExprU{F_\ominus}{E} }

\inferrule[T-Binary]
{\Gamma\vdash \xi_1 : E_1 \\ \Gamma\vdash \xi_2 : E_2}
{\Gamma\vdash \xi_1 \oplus \xi_2 : \ExprB{F_\oplus}{E_1}{E_2} }

%\inferrule[T-Binary-Const-Left]
%{\Gamma\vdash \xi : E \\ \Gamma\vdash c : T}
%{\Gamma\vdash c \oplus \xi : \ExprB{F_\oplus}{\Value{T}}{E} }

%\inferrule[T-Binary-Const-Right]
%{\Gamma\vdash \xi : E \\ \Gamma\vdash c : T}
%{\Gamma\vdash \xi \oplus c : \ExprB{F_\oplus}{E}{\Value{T}} }

\inferrule[T-Function]
{\Gamma\vdash \xi_1 : E_1 \\ \cdots \\ \Gamma\vdash \xi_k : E_k}
{\Gamma\vdash \varphi(\xi_1,\cdots,\xi_k) : \ExprK{F_\varphi}{E_1}{E_k} }

\inferrule[T-Guard]
{\Gamma\vdash \pi : E_1 \\ \Gamma\vdash \xi : E_2}
{\Gamma\vdash \pi \models \xi : \Guard{E_1}{E_2} }

\inferrule[T-Constructor]
{\Gamma\vdash \varpi_1 : E_1 \\ \cdots \\ \Gamma\vdash \varpi_k : E_k}
{\Gamma\vdash \mathsf{match}\langle T\left[,l\right]\rangle(\varpi_1,\cdots,\varpi_k) : \Cnstr{T\left[,l\right]}{E_1}{E_k} }

%\inferrule[T-Extended-Pattern]
%{ \varpi = \pi \\ \Gamma\vdash \pi : E}
%{\Gamma\vdash \varpi : E}

%\inferrule[T-Extended-Value]
%{ \varpi = c \\ \Gamma\vdash c : T}
%{\Gamma\vdash \varpi : \Value{T}}

%\inferrule[T-Extended-Var]
%{ \varpi = x \\ \Gamma\vdash x : T}
%{\Gamma\vdash \varpi : \Variable{T}}

\end{mathpar}
\caption{Typing rules for our pattern-matching SELL}
\label{typing}
\end{figure}

Figure~\ref{typing} shows rules we use to type expressions in our SELL. The 
types presented are not necessarily the exact C++ types we use to encode them, 
but we keep the correspondence as close as possible to reflect the actual 
implementation. We use the following type constructors, indicated with their 
arity: $\CWildcard^0$, $\CValue^1$, $\CVariable^1$, $\CExpr^{1+n}$, $\CGuard^2$, 
$\CCnstr^{1+n}$. We assume that type variables $T_i$ range over any C++ types, 
while $E_i$ only range over types marked with these type constructors, to which 
we refer as \emph{SELL-types}.

The judgments are of the traditional form $\Gamma\vdash \varpi : E$ that can be 
interpreted as given a typing environment $\Gamma$, an extended pattern $\varpi$ is 
given a SELL-type $E$. $\Gamma$ represents the typing context of the C++ 
compiler with the allowance for our simplified representation of SELL-types.
Types $F_\oplus$, $F_\ominus$ and $F_\varphi$ are described in greater details 
in \textsection\ref{sec:sem}, while for the purpose of typing they can be 
interpreted as types that uniquely identify operations $\oplus$, $\ominus$ and 
$\varphi$ respectively.

To avoid confusion we would like to point out that syntactic categories $\chi$, 
$\varsigma$ and $\_$ are defined as objects of C++ types \code{value<T>}, 
\code{variable<T>} and \code{wildcard}, while here we type them with SELL-types 
$\Value{T}$, $\Variable{T}$ and $\Wildcard$. Internally these types are the same 
of course.

\subsection{Semantics}
\label{sec:sem}

We use natural semantics\cite{Kahn87} (big-step operational semantics) to 
describe our pattern-matching semantics. As with syntax, we do not formalize the 
semantics of the entire language, but concentrate only on presenting relevant 
parts of our extension. We assume the entire state of the program is modeled by 
an environment $\Gamma$, which we can query as $\Gamma(x)$ to get a value of a 
variable $x$. In addition to meta-variables we have seen already, metavariables 
$u,v$ and $b^{bool}$ range over values. We make a simplifying assumption that 
all values of user-defined types are represented via variables of reference 
types and there exist a non-throwing operation \DynCast{\tau}{v} that can test 
whether an object of a given type is an instance of another type, returning a 
proper reference to it or a dedicated value \nullptr{} that represents 
\code{nullptr}. Intuitively, the semantics of such references is that of 
pointers in C++, which are implicitly dereferenced. We describe our semantics 
with several rule sets that deal with different parts of our syntax.

Because our SELL can be customized in a number of 
ways, we make use of several semantic functors that let the user define the 
semantics of the following operations:

\begin{compactitem}
\setlength{\itemsep}{0pt}
\setlength{\parskip}{0pt}
\item Type casting: $F_{dc}(\tau,v)$
\item Lazily evaluated functions: $F_\oplus,F_\ominus,F_\varphi$
\item Structural decomposition: $\Delta_i^{\tau,l}$
\item Algebraic decomposition: $\mathsf{solve}(\eta,v)$
\end{compactitem}

\noindent
The type of the subject used in pattern matching is not always the same as the 
type that a given pattern expects. The library in such a case may need to 
perform type casting of the subject, which may involve but is not limited to 
down-casting, up-casting, cross-casting or conversion. Depending on the types 
involved, such casting can be performed in different ways, which is why we 
abstract from a concrete semantics of such an operation with functor $F_{dc}$. 
We use the notation $F_{dc}(\tau,v)$ to refer to the result of casting value $v$ 
to target type $\tau$, which may result in a dedicated value $\nullptr$ that 
indicates impossibility of such a cast. We discuss various implementations of 
such a functor in \textsection\ref{sec:unisyn}.

Every function $\varphi$ that the user would like to be able to call lazily 
requires definition of a functor $F_\varphi$ that defines the semantics of such 
operation on any given argument types. The library defines such semantic objects 
$F_\oplus$ and $F_\ominus$ for every binary operation $\oplus$ and unary 
$\ominus$ it supports. The user is responsible for defining semantic functor 
$F_\varphi$ for every function $\varphi$ she would like to be able to evaluate 
lazily or use in a generalized n+k pattern. We show how to define such functors 
in \textsection\ref{sec:impl}, while here we use the notation $F(v_1,\cdots,v_k)$ 
to refer to the value representing the result of applying such a functor to 
values $v_1,\cdots,v_k$.

Each variant of an algebraic data type in a functional language has exactly one 
constructor, which makes it ideally suitable for structural decomposition of the 
type with pattern matching. Classes in C++ are allowed to have multiple 
constructors, which is why we need a mechanism that would let the user specify 
structural decomposition of a class. We do this with the help of bindings 
(\textsection\ref{sec:bnd}) represented here with a functor $\Delta_i^{\tau,l}$. 
We use the notation $\Delta_i^{\tau,l}(v)$ to refer to the value representing 
the $i^{th}$ component in layout $l$ of the structural decomposition of a value 
$v$ of type $\tau$.

Lastly, we let the user define the exact meaning of matching a value $v$ against 
an expression $\eta$ by case analysis on the structure of $\eta$. The exact 
details of defining such algebraic decomposition are given in 
\textsection\ref{sec:slv}, while here we use the notation $\mathsf{solve}(\eta,v)$ 
to refer to a boolean value indicating whether the generalized n+k pattern 
$\eta$ was accepted (true) or rejected (false).

We model the run-time environment of our SELL as a map $\Sigma: \chi\rightarrow T$ 
since our variables $\chi$ either hold a value of type \code{T} or refer to another 
variable of that type. In addition to meta-variables we have seen already, 
meta-variables $u,v$ and $b^{bool}$ range over values.

%\subsubsection{Evaluation Rules}
%\label{sec:eval}

\begin{figure}[h]
\begin{mathpar}

\inferrule[E-Value]
{\varsigma = \Value{\tau}(v)}
{\varsigma \lazyevals v}

\inferrule[E-Var]
{\chi = \Variable{\tau}(v)}
{\chi \lazyevals v}

\inferrule[E-Unary]
{\xi \lazyevals v}
{\ominus \xi \lazyevals F_\ominus(v)}

\inferrule[E-Binary]
{\xi_1 \lazyevals v_1 \\ \xi_2 \lazyevals v_2}
{\xi_1 \oplus \xi_2 \lazyevals F_\oplus(v_1,v_2)}

%\inferrule[E-Binary-Const-Left]
%{\xi \lazyevals v}
%{\xi \oplus c \lazyevals F_\oplus(v,c)}

%\inferrule[E-Binary-Const-Right]
%{\xi \lazyevals v}
%{c \oplus \xi \lazyevals F_\oplus(c,v)}

\inferrule[E-Function]
{\xi_1 \lazyevals v_1 \\ \cdots \\ \xi_k \lazyevals v_k}
{\varphi(\xi_1,\cdots,\xi_k) \lazyevals F_\varphi(v_1,\cdots,v_k)}

\end{mathpar}
\caption{Evaluation rules}
\label{evaluation}
\end{figure}

Figure~\ref{evaluation} shows the evaluation rules used to evaluate lazy expressions 
that our SELL introduces. The judgments are of the form $\Sigma\vdash \xi \lazyevals v$ 
stating that lazy expression $\xi$ evaluates to a value $v$ in a run-time 
environment $\Sigma$. We do not mention the run-time environment in the rules 
for brevity since the evaluation does not modify it.

\subsubsection{Semantics of Matching Expressions}
\label{sec:semme}

\begin{figure}[h]
\begin{mathpar}
\inferrule[P-Wildcard]
{}
{\Sigma\vdash \_(v_e) \evals \True,\Sigma}

\inferrule[P-Value]
{\varsigma \lazyevals u}
{\Sigma\vdash \varsigma^\tau(v_e) \evals (u=v),\Sigma}

\inferrule[P-Variable]
{u=F_{dc}(\tau,v_e)}
{\Sigma\vdash \chi^{\tau}(v_e) \evals (u \neq \nullptr{}),\Sigma[\chi\leftarrow u]}

\inferrule[P-n+k-Pattern]
{\Sigma\vdash \mathsf{solve}(\xi,v_e) \evals v,\Sigma'}
{\Sigma\vdash \xi(v_e) \evals v,\Sigma'}

\inferrule[P-Guard]
{\Sigma\vdash \pi(v_e) \evals b_\pi,\Sigma' \\ \Sigma'\vdash \xi \lazyevals b_\xi}
{\Sigma\vdash (\pi \models \xi)(v_e) \evals (b_\pi \wedge b_\xi),\Sigma'}

\inferrule[P-Constructor-Nullptr]
{F_{dc}(\tau,v_e)=\nullptr{}}
{\Sigma\vdash (\mathsf{match}\langle\tau\left[,l\right]\rangle(\varpi_1,...,\varpi_k))(v_e) \evals \False,\Sigma}

\inferrule[P-Constructor-Reject]
{ u=F_{dc}(\tau,v_e) \\
 \Sigma_1    \vdash \varpi_1(\Delta_1^{\tau,l}(u))         \evals \True, \Sigma_2 \\ \cdots \\
 \Sigma_{i-1}\vdash \varpi_{i-1}(\Delta_{i-1}^{\tau,l}(u)) \evals \True, \Sigma_i \\
 \Sigma_i    \vdash \varpi_i(\Delta_i^{\tau,l}(u))         \evals \False,\Sigma_{i+1}
}
{\Sigma\vdash (\mathsf{match}\langle\tau\left[,l\right]\rangle(\varpi_1,...,\varpi_k))(v_e) \evals \False,\Sigma_{i+1}}

\inferrule[P-Constructor-Accept]
{ u=F_{dc}(\tau,v_e) \\
 \Sigma_1    \vdash \varpi_1(\Delta_1^{\tau,l}(u)) \evals \True, \Sigma_2 \\ \cdots \\
 \Sigma_k    \vdash \varpi_k(\Delta_k^{\tau,l}(u)) \evals \True, \Sigma_{k+1}
}
{\Sigma\vdash (\mathsf{match}\langle\tau\left[,l\right]\rangle(\varpi_1,...,\varpi_k))(v_e) \evals \True,\Sigma_{k+1}}

\end{mathpar}
\caption{Semantics of matching expressions}
\label{exprsem}
\end{figure}

The rule set in Figure~\ref{exprsem} deals with pattern application $\pi(e)$, 
which essentially performs matching of a pattern $\pi$ against an expression 
$e$. To avoid dealing with the C++ semantics, we assume that the expression $e$ 
has already been evaluated to a value $v_e$. Our judgments are thus of the 
form $\Sigma\vdash \pi(v_e) \evals v,\Sigma'$ that can be interpreted as 
following: given an environment $\Sigma$ and a value $v_e$ representing the 
result of evaluating subject expression $e$ according to the C++ semantics, 
pattern application $\pi(v_e)$ results in value $v$ and environment $\Sigma'$. 

Matching a wildcard pattern against expression always succeeds without changes 
to the environment (\RefTirName{Wildcard}). Matching a value pattern against 
expression succeeds only if the result of evaluating that expression is the same 
as the constant (\RefTirName{Value}). Matching against variable will always 
succeeds when the type of expression $e$ is the same as variable's value type 
$\tau$. When the types are different, the library will try to use 
\code{dynamic_cast<}$\tau$\code{>(e)} to see whether dynamic type of expression 
can be casted to $\tau$. If it does, matching succeeds, binding variable to the 
result of \code{dynamic_cast}. If it does not, matching fails 
(\RefTirName{Variable}).

Our semantics for generalized n+k patterns draws on the notion of 
\emph{backward collecting semantics} used in \emph{abstract 
interpretation}\cite{CousotCousot92-1}. In general, backward collecting 
semantics $Baexp\Sem{A}(E)R$ of an expression $A$ defines the subset of 
possible environments $E$ such that the expression may evaluate, without 
producing a runtime error, to a value belonging to given set $R$:

\begin{lstlisting}
@$Baexp\Sem{A}(E)R = \{x \in E | A(x) \in R\}$@
\end{lstlisting} 

This can be interpreted as following: given a set $E$ from where the arguments 
of an expression $A$ draw their values, as well as a set $R$ of acceptable (not 
all possible) results, find the largest subset $X \subseteq E$ of arguments that 
will only render results of evaluating $A$ on them in $R$.

Intuitively n+k patterns like $f(x,y)=v$ relate a known result of a given 
function application to its arguments (hence analogy with backward collecting 
semantics). The case where multiple unknown arguments are matched against a 
single result should not be immediately discarded as there are known n-ary 
functions whose inverse is unique. An example of such function is Cantor pairing 
function that defines bijection between $\mathbb{N}\times\mathbb{N}$ and $\mathbb{N}$.
Even when such mappings are not one-to-one, their restriction to a given 
argument often is. Most generalizations of n+k patterns seem to agree on the 
following rules:

\begin{itemize}
\item Absence of solution that would result in a given value should be indicated 
      through rejection of the pattern.
\item Presence of a unique solution should be indicated with acceptance of the 
      pattern and binding of corresponding variables to the solution.
\end{itemize}

\noindent As to the case when multiple solutions are possible, several 
alternatives can be viable:

\begin{itemize}
\item Reject the pattern.
\item Accept, binding to either an arbitrary or some normalized solution.
\item When set of solutions is guaranteed to be finite -- accept, binding 
      solutions to a set variable.
\item When set of solutions is guaranteed to be enumerable -- accept, binding 
      solutions to a generator capable of enumerating them all.
\end{itemize}

\noindent
We believe that depending on application, any of these semantic choices can be 
valid, which is why we prefer not to make such choice for the user, but rather 
provide him with means to decide himself. This is why our semantics for matching 
against generalized n+k pattern depends on a family of user-defined functions 

\begin{lstlisting}
@$\Psi_f^\tau:\tau_r\times\tau_1\times...\times1\times...\times\tau_k\rightarrow bool\times\tau$@
\end{lstlisting} 

\noindent
such that $\Psi_f^\tau[r](c_1,...,\bullet,...,c_k)$ for a given function 

\begin{lstlisting}
@$f:\tau_1,...,\tau,...,\tau_k\rightarrow\tau_r$@
\end{lstlisting} 

\noindent should return a pair composed of a boolean indicating acceptance of a 
pattern $f(c_1,...,x^\tau,...,c_k)=r$ and a solution with respect to $x$ 
when the match was reported successful. Symbol $\bullet$ indicates a position in 
the argument list for which a solution is sought, the rest of the arguments are 
known values. We describe how user can supply the function $\Psi_f^\tau$ for his 
own operation $f$ in \textsection\ref{sec:slv}.

The only difference between the three rules defining semantics of n+k patterns 
is the arity of the root operator and the position in the argument list in which 
the only non-value pattern was spotted (\RefTirName{n+k Binary Left}, 
\RefTirName{n+k Binary Right} and \RefTirName{n+k Unary}). We use user-defined 
$\Psi_f^\tau$ to solve for a given argument of a given operator and then recurse 
to match corresponding sub-expression. Note that when user did not provide 
$\Psi_f^\tau$ for the argument in which solution is sought, the rule is 
rejected.

Evaluation of a guard pattern first tries to match the left hand side of a guard 
expression, usually binding a variable in it, and then if the match was 
successful, lazily evaluates its right hand side to make sure the new value of 
the bound variable is used. The result of evaluating the right hand side 
converted to \code{bool} is reported as the result of matching the entire 
pattern (\RefTirName{Guard}).

Matching of a tree patterns begins with evaluating subject expression and 
casting it dynamically to target type $\tau$ when subject type is not $\tau$. 
When \code{dynamic_cast} fails returning \code{nullptr}, the pattern is rejected 
(\RefTirName{Tree-Nullptr}). Once a value of a target type has been uncovered, 
we proceed with matching arguments left-to-right. For each argument we first 
translate \emph{extended pattern} $\omega$ accepted by tree pattern into an 
\emph{application pattern} $\pi$ to get rid of the syntactic convenience we 
allow on arguments of tree patterns. Using the target type and optional layout 
that was provided by the user, we obtain a value that should be bound in the 
$i^{th}$ position of decomposition. Again we rely on family of user provided 
functions $\Delta_i^{\tau,l}(u)$ that take an object instance and returns a 
value bound in the $i^{th}$ position of its $l^{th}$ layout. Specification of 
function $\Delta$ by the user is discussed in~\textsection\ref{sec:bnd}. Here we 
would like to point out however that the number of argument patterns passed over 
to the tree pattern could be smaller than the number of binding positions defined 
by specific layout. Remaining argument positions are implicitly assumed to be 
filled with the wildcard pattern.

When we have the value for the $i^{th}$ position of object's decomposition, we 
match it against the pattern specified in the $i^{th}$ position and if the value 
is accepted we move on to matching the next argument (\RefTirName{Tree-False}). 
Only in case when all the argument patterns have been successfully matched the 
matching succeeds by returning a pointer to the target type, which in C++ can be 
used everywhere a boolean expression is expected. Returning pointer instead of 
just boolean value gives us functionality similar to that of \emph{as 
patterns} while maintaining the composibility with the 
rest of the library (\RefTirName{Tree-True}).

%\subsubsection{Semantics of Match Statement}
%\label{sec:semms}

\begin{figure}[h]
\begin{mathpar}
\inferrule[Match-True]
{ v_e \neq \nullptr \\
 \Sigma      \vdash_{v_e} C_1    \evals \False,\Sigma_1     \\ \cdots \\
 \Sigma_{i-2}\vdash_{v_e} C_{i-1}\evals \False,\Sigma_{i-1} \\
 \Sigma_{i-1}\vdash_{v_e} C_i    \evals \True, \Sigma_i
}
{\Sigma\vdash \mathsf{Match}(v_e) \{ \left[C_i \vec{s}_i\right]^*_{i=1..n} \} \mathsf{EndMatch} \evals i,\Sigma_i}

\inferrule[Match-False]
{ v_e \neq \nullptr \\
 \Sigma      \vdash_{v_e} C_1    \evals \False,\Sigma_1 \\ \cdots \\
 \Sigma_{n-1}\vdash_{v_e} C_n    \evals \False,\Sigma_n
}
{\Sigma\vdash \mathsf{Match}(e) \{ \left[C_i \vec{s}_i\right]^*_{i=1..n} \} \mathsf{EndMatch} \evals 0,\Sigma_n}

\inferrule[Qua]
{\Sigma \vdash \mathsf{match}\langle\tau,l\rangle(\vec{\varpi})(v_e) \evals b,\Sigma' }
{\Sigma \vdash_{v_e} \mathsf{Qua}(\tau,\vec{\varpi}) \evals b,\Sigma'[\mathsf{matched}^\tau\rightarrow F_{dc}(\tau,v_e)]}

\inferrule[When]
{\Sigma \vdash_{v^\tau_e} \mathsf{Qua}(\tau,\vec{\varpi}) \evals b,\Sigma'}
{\Sigma \vdash_{v^\tau_e}     \mathsf{When}(\vec{\varpi}) \evals b,\Sigma'}

\inferrule[Case]
{\Delta_i^\tau : \tau \rightarrow \tau_i, i=1..k \\
 \Sigma[x_i^{\tau_i}\rightarrow\nullptr]_{i=1..k} \vdash_{v_e} \mathsf{Qua}(\tau,x_1,...,x_k) \evals u,\Sigma' }
{\Sigma \vdash_{v_e} \mathsf{Case}(\tau,x_1,...,x_k) \evals u,\Sigma'}

\inferrule[Otherwise]
{\Sigma \vdash_{v^\tau_e} \mathsf{Case}(\tau,\vec{x}) \evals u,\Sigma'}
{\Sigma \vdash_{v^\tau_e} \mathsf{Otherwise}(\vec{x}) \evals u,\Sigma'}
\end{mathpar}
\caption{Semantics of match-statement}
\label{stmtsem}
\end{figure}

The rule set in Figure~\ref{stmtsem} describes the semantics of a \emph{match 
statement}. In order to avoid dealing with the semantics of the C++ statements, 
we define the semantics of a match-statement to be the index of the matching case 
clause and the run-time environment right before the clause's statement, or $0$ 
if none of the clauses matched. The judgments are thus of the form 
$\Sigma\vdash M \evals v,\Sigma'$ for match statement, and are slightly extended 
for case clauses $\Sigma\vdash_{v_e} C \evals b,\Sigma'$ with value $v_e$ of a 
subject that is passed along from the match statement onto the clauses.

The rules essentially describe the first-fit strategy for evaluating the clauses.
Evaluation of a \code{Qua}-clause is equivalent to evaluation of a corresponding 
match-expression on a constructor pattern. Successful match will introduce into 
the local scope of the clause a variable \code{matched} bound to the subject 
properly casted to the target type $\tau$. Evaluation of \code{When}-clause 
amounts to evaluation of a corresponding \code{Qua}-clause with target type 
being the subject type. Evaluation of \code{Case}-clauses amounts to evaluation 
of \code{Qua}-clauses in the environment extended with variables passed as 
arguments to the clause. Evaluation of default clause amounts to evaluating a 
corresponding \code{Case}-clause with target type being the subject type.

Evaluation of a match statement begins with evaluation of subject expression, 
which is not allowed to result in \code{nullptr}. This value is passed along to 
each of the clauses. The clauses are evaluated in their lexical order until the
first one that is not rejected. Statements associated with it are evaluated to 
form the outcome of the match statement. The resulting environment makes sure 
that local variables introduced by case clauses are not available after the 
match statement (\RefTirName{Match-True}). When none of the clauses were 
accepted, which is only possible when default clause was not specified, the 
resulting environment might still be different from the initial environment 
because of variables bound in partial matches during evaluation of clauses 
(\RefTirName{Match-False}).

Evaluation of a \code{Qua}-clause is equivalent to evaluation of a corresponding 
match-expression on a tree pattern. Successful match will introduce a variable 
\code{matched} of type $\tau\&$ that is bound to subject properly casted to the 
target type $\tau$ into the local scope of the clause.

Evaluation of \code{Case}-clauses amounts of evaluation of \code{Qua}-clauses in 
the environment extended with variables passed as arguments to the clause. The 
variables introduced by the \code{Case}-clause have the static type of values 
bound in corresponding positions, which ensures that variable patterns will be 
irrefutable (\RefTirName{Case}). In practice, the variables are of reference 
type so that no unnecessary copying is happening.

Evaluation of default clause cannot fail because there is no \code{dynamic_cast} 
involved neither for the subject nor for implicit local variables: for the 
former the target type is by definition the subject type, while for the latter 
the type is chosen to be the type of expected values (\RefTirName{Otherwise}).